Traced monoidal category

In category theory, a traced monoidal category is a category with some extra structure which gives a reasonable notion of feedback.

A traced symmetric monoidal category is a symmetric monoidal category C together with a family of functions

$\mathrm{Tr}^U_{X,Y}:\mathbf{C}(X\otimes U,Y\otimes U)\to\mathbf{C}(X,Y)$

called a trace, satisfying the following conditions:

$\mathrm{Tr}^U_{X,Y}(f)g=\mathrm{Tr}^U_{X',Y}(f(g\otimes U))$

$g\mathrm{Tr}^U_{X,Y}(f)=\mathrm{Tr}^U_{X,Y'}((g\otimes U)f)$

$\mathrm{Tr}^U_{X,Y}((Y\otimes g)f)=\mathrm{Tr}^{U'}_{X,Y}(f(X\otimes g))$

$\mathrm{Tr}^I_{X,Y}(f)=f$

$\mathrm{Tr}^{U\otimes V}_{X,Y}(f)=\mathrm{Tr}^U_{X,Y}(\mathrm{Tr}^V_{X\otimes U,Y\otimes U}(f))$

$g\otimes \mathrm{Tr}^U_{X,Y}(f)=\mathrm{Tr}^U_{W\otimes X,Z\otimes Y}(g\otimes f)$

$\mathrm{Tr}^U_{U,U}(\gamma_{U,U})=U$

(where $\gamma$ is the symmetry of the monoidal category).

Properties

Given a traced monoidal category C, the Int construction generates the free (in some bicategorical sense) compact closure Int(C) of C.

André Joyal, Ross Street, Dominic Verity (1996). "Traced monoidal categories". Mathematical Proceedings of the Cambridge Philosophical Society 3: 447–468. doi:10.1017/S0305004100074338.